$\forall$${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}, $p$:(\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$Prop).
\\[0ex]$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$$e$ = first $e$ $\geq$ $e_{1}$.$p$($e$) $\Leftrightarrow$ $\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$$p$($e$)